\newcommand{\ignore}[1]{}
\newcommand{\fix}[1]{\textcolor{red}{$^\star$}\marginpar{\scriptsize\flushleft \textcolor{red}{#1}}}
\newcommand{\todo}[1]{\begin{quote}\sffamily\textcolor{red}{``#1''}\end{quote}}


\newenvironment{Case}[1]{\noindent(#1)}{}


\newcommand{\set}[1]{\{#1\}}
\newcommand{\Set}[1]{\big\{#1\big\}}
\newcommand{\setx}[2]{\{#1\mid#2\}}
\newcommand{\Setx}[2]{\big\{#1\mid#2\big\}}
\newcommand{\tup}[1]{\left\langle#1\right\rangle}

\renewcommand{\phi}{\varphi}
\renewcommand{\epsilon}{\varepsilon}

% abbreviations like \calA, \calB, ...
\makeatletter

% \create@abbrev{<abrev>}{<font>}{<characters>}
% creates abbreviations \<abbrev><X> evaluating to \<font> <X> for each characte
%   <X> in <characters>
\def\create@abbrev#1#2#3{
  \def\c@a@def##1{
      \if ##1.
        \relax
      \else
        \@ifdefinable{\@nameuse{#1##1}}{\@namedef{#1##1}{#2##1}}
        \expandafter\c@a@def
      \fi
    }
  \c@a@def #3.
}

\create@abbrev{cal}{\mathcal}{ABCDEFGHIJKLMNOPQRSTUVWXYZ}
\create@abbrev{frak}{\mathfrak}{ABCDEFGHIJKLMNOPQRSTUVWXYZ}
\create@abbrev{bb}{\mathbb}{ABCDEFGHIJKLMNOPQRSTUVWXYZ}
\create@abbrev{tt}{\mathtt}{ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz}
\create@abbrev{rm}{\mathrm}{ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz}
\create@abbrev{sf}{\mathsf}{ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz}
\create@abbrev{ol}{\overline}{ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz}

\create@abbrev{aut}{\mathcal}{ABCDEFGHIJKLMNOPQRSTUVWXYZ}

\makeatother




% ----------------------------------------------------------------------
% abbreviations for this document 
% ----------------------------------------------------------------------
\newcommand{\fst}[1]{\tup{#1}_1}
\newcommand{\snd}[1]{\tup{#1}_2}


% --------------------------------
% |          Automaton           |
% --------------------------------
\newcommand{\qacc}{q_{acc}}
\newcommand{\qrej}{q_{rej}}
%\renewcommand{\sharp}{\#}
\newcommand{\nsharp}{G\neg\#}
\newcommand{\oI}{o_{I}}
\newcommand{\pI}{p_{I}}
\newcommand{\qI}{q_{I}}

\newcommand{\minmodels}{\mathbin{|\hspace{-1.6mm}\equiv}}
\newcommand{\notminmodels}{\mathbin{|\hspace{-1.6mm}\not\equiv}}
\newcommand{\snf}{\thanks{Supported by the Swiss National Science Foundation (SNF). \today}}



% --------------------------------
% |          PSL SYNTAX          |
% --------------------------------
\newcommand{\true}{\ensuremath{\mathsf{tt}}}
\newcommand{\false}{\ensuremath{\mathsf{ff}}}
\newcommand{\sub}[1]{\mathop{Sub(#1)}}

% \DeclareSymbolFont {<sym-font-name>} {<encoding>} {<family>}  {<series>} {<shape>} 
% http://tex.loria.fr/general/new/fntguide.html
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}  
\DeclareMathSymbol{\diamondleft}{\mathrel}{symbolsC}{134}
\DeclareMathSymbol{\diamondright}{\mathrel}{symbolsC}{132}
\DeclareMathSymbol{\boxleft}{\mathrel}{symbolsC}{130}
\DeclareMathSymbol{\boxright}{\mathrel}{symbolsC}{128}

\newcommand{\starto}{\ensuremath{\mathbin{\star\!\!\!\to}}}


% core PSL
\newcommand{\opX}{\ensuremath{\mathsf{X}}}
\newcommand{\opY}{\ensuremath{\mathsf{Y}}}
\newcommand{\opU}{\ensuremath{\mathbin{\mathsf{U}}}}
\newcommand{\opS}{\ensuremath{\mathbin{\mathsf{S}}}}
\newcommand{\fby}{\ensuremath{\mathbin{\diamondright}}}  
\newcommand{\bfby}{\ensuremath{\mathbin{\pmb-\hspace{-2.5ex}\diamondright}}}  
\newcommand{\cl}{\ensuremath{\mathsf{cl}}}


% syntactic sugar
\newcommand{\opZ}{\ensuremath{\mathsf{Z}}}
\newcommand{\opR}{\ensuremath{\mathbin{\mathsf{R}}}}
\newcommand{\opF}{\ensuremath{\mathsf{F}}}
\newcommand{\opG}{\ensuremath{\mathsf{G}}}
\newcommand{\trig}{\ensuremath{\mathbin{\boxright}}}  

\newcommand{\opT}{\ensuremath{\mathbin{\mathsf{T}}}}
\newcommand{\opO}{\ensuremath{\mathsf{O}}}
\newcommand{\opH}{\ensuremath{\mathsf{H}}}
\newcommand{\btrig}{\ensuremath{\mathbin{\pmb-\hspace{-2.5ex}\boxright}}}  
